| 1: | minus(x,0) | → x | |
| 2: | minus(s(x),s(y)) | → minus(x,y) | |
| 3: | le(0,y) | → true | |
| 4: | le(s(x),0) | → false | |
| 5: | le(s(x),s(y)) | → le(x,y) | |
| 6: | quot(x,s(y)) | → if_quot(le(s(y),x),x,s(y)) | |
| 7: | if_quot(true,x,y) | → s(quot(minus(x,y),y)) | |
| 8: | if_quot(false,x,y) | → 0 | |
| 9: | MINUS(s(x),s(y)) | → MINUS(x,y) | |
| 10: | LE(s(x),s(y)) | → LE(x,y) | |
| 11: | QUOT(x,s(y)) | → IF_QUOT(le(s(y),x),x,s(y)) | |
| 12: | QUOT(x,s(y)) | → LE(s(y),x) | |
| 13: | IF_QUOT(true,x,y) | → QUOT(minus(x,y),y) | |
| 14: | IF_QUOT(true,x,y) | → MINUS(x,y) | |